package tr.edu.ege.kipler.satisfiability.container;

import java.util.HashSet;
import java.util.Set;
import java.util.Stack;

import tr.edu.ege.kipler.common.Copyable;
import tr.edu.ege.kipler.common.MultivalueHashMap;
import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.syntax.Role;
import tr.edu.ege.kipler.syntax.WorldElement;
import tr.edu.ege.kipler.syntax.atomicformula.RoleAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.RoleInclusion;
import tr.edu.ege.kipler.syntax.atomicformula.RoleAssertion.Type;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class RBox implements FormulaBase, Copyable<RBox> {

	private MultivalueHashMap<Role, Role> inclusions = new MultivalueHashMap<Role, Role>();

	private MultivalueHashMap<Type, Role> assertions = new MultivalueHashMap<Type, Role>();

	private Set<RoleInclusion> negInclusions = new HashSet<RoleInclusion>();

	public void add(RoleInclusion ri) {
		if (ri.isNegated()) {
			negInclusions.add(ri);
		} else {
			inclusions.put(ri.getRhs(), ri.getLhs());
			inclusions.put(ri.getRhs().copy().toggleInverse(), ri.getLhs()
					.copy().toggleInverse());
		}

	}

	public void add(RoleAssertion ra) {
		assertions.put(ra.getType(), ra.getRole());
		assertions.put(ra.getType(), ra.getRole().copy().toggleInverse());
	}

	public void add(WorldElement formula) throws UnsatisfiableException {
		if (formula instanceof RoleInclusion) {
			add((RoleInclusion) formula);
		} else if (formula instanceof RoleAssertion) {
			add((RoleAssertion) formula);
		}
	}

	public Set<Role> getSubRoles(Role role) {
		Set<Role> result = new HashSet<Role>();
		Stack<Role> state = new Stack<Role>();
		state.push(role);
		while (!state.isEmpty()) {
			// TODO check duplicate values in the stack
			Role currRole = state.pop();
			if (!result.contains(currRole)) {
				result.add(currRole);
				state.addAll(inclusions.getValuesForKey(currRole));
			}
		}
		return result;
	}

	public Set<Role> getEqualRoles(Role role) {
		Set<Role> result = new HashSet<Role>();
		for (Role subRole : getSubRoles(role)) {
			if (getSubRoles(subRole).contains(role)) {
				result.add(subRole);
			}
		}
		return result;
	}

	public Set<RoleInclusion> getNegatedInclusions() {
		return negInclusions;
	}

	public boolean contains(WorldElement formula) {
		boolean result = false;
		if (formula instanceof RoleInclusion) {
			RoleInclusion ri = (RoleInclusion) formula;
			if (ri.isNegated()) {
				result = getNegatedInclusions().contains(ri);
			} else {
				result = getSubRoles(ri.getRhs()).contains(ri.getLhs());
			}
		} else if (formula instanceof RoleAssertion) {
			RoleAssertion ra = (RoleAssertion) formula;
			result = isTransitiveRole(ra.getRole());
		}
		return result;
	}

	private boolean isTransitiveRole(Role role) {
		boolean result = false;
		Set<Role> transitiveRoles = assertions.getValuesForKey(Type.TRANSITIVE);
		for (Role equalRole : getEqualRoles(role)) {
			if (transitiveRoles.contains(equalRole)
					|| transitiveRoles.contains(equalRole.copy()
							.toggleInverse())) {
				result = true;
				break;
			}
		}
		return result;
	}

	public Set<WorldElement> getFormulas() {
		Set<WorldElement> result = new HashSet<WorldElement>();
		for (Role superRole : inclusions.keySet()) {
			for (Role subRole : inclusions.getValuesForKey(superRole)) {
				result.add(new RoleInclusion(subRole, superRole));
			}
		}
		for (RoleInclusion ri : negInclusions) {
			result.add(ri);
		}
		for (Role transitiveRole : assertions.getValuesForKey(Type.TRANSITIVE)) {
			result.add(new RoleAssertion(Type.TRANSITIVE, transitiveRole));
		}
		return result;
	}

	public boolean isSatisfiable() {
		return true;
	}

	@Override
	public boolean equals(Object obj) {
		if (obj != null && (obj.getClass().equals(this.getClass()))) {
			RBox other = (RBox) obj;
			return inclusions.equals(other.inclusions)
					&& negInclusions.equals(other.negInclusions)
					&& assertions.equals(other.assertions);
		}
		return false;
	}

	public RBox copy() {
		RBox result = new RBox();
		result.inclusions = inclusions.copy();
		result.assertions = assertions.copy();
		result.negInclusions = new HashSet<RoleInclusion>(negInclusions);
		return result;
	}

	@Override
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		buffer.append("RBox");
		buffer.append(" = {");
		for (WorldElement f : getFormulas())
			buffer.append(f + ", ");
		buffer.delete(buffer.length() - 2, buffer.length());
		buffer.append("}");
		return buffer.toString();
	}

}
